/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.bool;
import java.io.BufferedReader;
import java.io.File;
import java.io.FileReader;
import java.io.IOException;
import java.io.LineNumberReader;
import java.util.HashSet;
import java.util.Iterator;
import java.util.Set;

import alloy.util.Dbg;
import alloy.util.EnvFailureException;
import alloy.util.FileUtil;
import alloy.util.Msg;
import alloy.util.Params;
import alloy.util.ProcessInfo;
import alloy.util.ResourceManager;
import alloy.util.SetOfLong;
import alloy.util.TmpFiles;

/**
 * BLSATLab: Java interface to SatLab, which is (among other things) a uniform
 * interface to SAT solvers, written in C++.
 * A particular backend - extends BLBackend.
 * Actual work is done by a native program called SatLab;
 * below, we refer to it as "the solver".  SatLab actually is a front-end
 * for several satisfiability solvers which lets us set their parameters
 * and ask them to solve .sat instances and read results in a uniform manner.
 */
public class BLSATLab extends BLBackend {

    /** The currently running process: either sat2cnf conversion or sat solver. */
    private SATProcessInfo _process;

    /** Whether {@link #solve} or {@link #next} is in progress.
      Currently the code is non-reentrant: once we start
      solving one formula, we cannot start solving another
      until this one either finishes or is cancelled.  There is no fundamental
      reason why this has to be so, but for now it is so for simplicity. */
    private boolean _solveInProgress = false;

    /** Whether "cancel solving" command is in progress,
      i.e. {@link #interruptSolver} has been called but
      the currently running {@link #solve} or {@link #next}
      has not yet returned. */
    private boolean _cancelInProgress = false;

    /** Number of Boolean variables in the last Boolean formula we were solving.
      Saved by {@link #_solve} to be used by {@link #_next}. */
    private int _lastNumVars;

    /** Name of solution file to which solutions are written by the solver.
      Saved by {@link #_solve} to be used by {@link #_next}. */
    private File _lastSolutionFileHandle;

    /**
    * Solution file reader from which we are reading solutions.
    * The maximum number of solutions in a file is given by
    * the global parameter MAIN.enumBatchSize.
    */
    private LineNumberReader _solReader;

    /** Name of the last .cnf file */
    private File _lastCnfFileHandle;

    /** Name of the last .sat file */
    private File _lastSatFileHandle;

    /**
     * Name of the last template instantiation file that says which literals in the _lastCnfFileName
     * instantiate which templates with which arguments.
     */
    private File _lastIstFileHandle;

    /////////////
    // Methods //
    /////////////

    /**
     * Constructor
     */
    BLSATLab() {
        Dbg.addDbgMsgListener(Dbg.FATAL, new Dbg.DbgMsgListener () {
            public void debugMsg(int msgType_, String msg_, Throwable thrown_) {
              _reset();
            }
            public void debugMsg(int msgType_, Msg msg_, Throwable thrown_) {
              _reset();
            }});
    }

    /**
     * Reset state for new solving, following a fatal error.
     */
    private void _reset() {
        _solveInProgress = false;
        _cancelInProgress = false;
    }

    /**
     * Find the unsatisfiable core of the last analyzed formula (assumed to be unsatisfiable).
     * The core is represented as a {@linkplain BoolStencil stencil} that says, for each Boolean
     * {@linkplain alloy.bool.BoolTemplateInstance#templCacheId template},
     * which {@linkplain alloy.bool.BoolTemplateInstance instances} of it are used in the core.
     * This routine returns an ArrayList where the i'th element
     * is a {@link SetOfLong} that holds the {@linkplain alloy.bool.BoolTemplateInstance#computeTemplKey instantiations}
     * of boolean template i that are in the core.
     * <p>
     * Now, note that this routine computes the unsat core in terms of the Boolean translation of the
     * AST.  What the user wants to see is an unsat core expressed in terms of the AST itself
     * (or even better -- in terms of the text of his original model, if possible).  To determine
     * whether a particular ground node is in the AST, we can get the {@link alloy.transl.Transl}ation of this
     * node to a vector of {@link BooleanFormula}s, look at the {@linkplain BooleanFormula#recordCachingInfo
     * Boolean template annotations} of these Boolean formulas, and {@linkplain BoolStencil#allows ask} the
     * {@link BoolStencil} returned by {@link #computeUnsatCore}
     * whether the
     * <p>
     * An explanation of unsatisfiable core extraction is given in the following paper:
     * I. Shlyakhter, R. Seater, D. Jackson, M. Sridharan, M. Taghdiri.
     * <a href="http://ilya.cc/ucore.ps">Debugging Overconstrained Declarative Models Using Unsatisfiable Cores</a>,
     * <a href="http://www.ase-conference.org">ASE</a> 2003.
     * <em>However</em>, the algorithm currently implemented (october 2003)
     * is not the same algorithms as described in the paper.  This is because we do not first compute a ground form of the
     * AST and then translate to CNF; we first translate to a lifted Boolean DAG and then ground out that DAG.  So the
     * mapping-back of unsat core is done differently.
     * <p>
     * @see http://ilya.cc/ucore.ps
     */
    protected BoolStencil _computeUnsatCore() {
    Dbg.chk(BLBackend.getLastResult() == BLBackend.BL_UNSAT);

    try {
		Dbg.info("Extracted unsat core...");

    		/*
         * Extract the unsatisfiable core of the .cnf file generated for the last analyzed formula.
         * The core is an unsatisfiable subset of the .cnf clauses.
         * To reduce the size of the core, we extract the core of the core until a fixed point
         */

		_extractingUnsatCore = true;
		boolean cnfGenerationFailed = false;
		try {
		    if (_solve(_ucore_formula, _ucore_nvars, _ucore_dependentVars, "ZCHAFF", false /* enum_ */, _ucore_randSeed,
			       BL_RUN_SOLVE, _ucore_primVarFileHandle) == BL_CANCELLED)
			cnfGenerationFailed = true;
		} catch (EnvFailureException ef_) {
		    cnfGenerationFailed = true;
		}
		_extractingUnsatCore = false;
		if (cnfGenerationFailed) {
		    Dbg.fatal("Error generating cnf for unsat core");
		    return null;
		}

        final File lastCnfFileHandle = BLBackend.getLastCnfFileHandle();
        //stop after numIterations iterations even if we have nto yet reached a fixed points
        int numIterations = Params.glob.getIntParam("DEVEL", "coreiter", 5);
        Dbg.chk(numIterations > 0); //we have to run it at least once

        // run the core extractor until we reach a fixedpoint
        // (or until the maximum number of iterations, numIterations)
        final File proofFileHandle = TmpFiles.createHandleToATempFile("proof.prf");
        int curIter = 0;
        File coreFileHandle = null;
        int lastClauseCount = 0;  //when the clause count doesn't change, we have reached a fixedpoint
        boolean iterationDone = false;
        //FileUtil.copy(lastCnfFileName, lastCnfFileName + "_iteration_0");
        File iterFileHandle = lastCnfFileHandle;
        do {
			int iterClauseCount = BoolUtil.getCnfNumClauses(iterFileHandle);
			if (iterClauseCount == lastClauseCount) {
				// reached a fixpoint; last core extraction did not reduce .cnf size
				iterationDone = true;
			} else {
				lastClauseCount = iterClauseCount;

				// core extraction involves two steps:
				//   -- running zchaff on the .cnf to produce a proof
				//      of unsatisfiability. the proof is a DAG showing
				//      how to derive an empty clause from the .cnf clauses
				//      via resolution.
				//   -- running zcore on the .cnf and the proof of
				//      unsatisfiability, to produce the unsat core
				//      (consisting of clauses that were used in the proof).

				try {
					final String[] args = { "-a",
							proofFileHandle.getName(),
							iterFileHandle.getName() };
					_process = new SATProcessInfo("zchaff", args, TmpFiles.getTmpDir());
				} catch (IOException ioe_) {
					Dbg.fatal("could not start zchaff", ioe_);
				}
				_process.runUntilOutcome();
				_killProcess();

				File nextIterFileHandle = new File(lastCnfFileHandle.getParent(),
						lastCnfFileHandle.getName() + "_iteration_" + (++curIter));
				final String[] args = { iterFileHandle.getName(),
						proofFileHandle.getName(),
						nextIterFileHandle.getName() };
				ProcessInfo.runTillEnd("zcore", args, TmpFiles.getTmpDir());

				iterFileHandle = nextIterFileHandle;
				coreFileHandle = iterFileHandle;
			}
		} while (!iterationDone && curIter < numIterations);

        /*
		 * Now we have the unsatisfiable core of the .cnf; we need to turn it
		 * into an unsatisfiable core of the ground DAG. We do this by treating
		 * the unsatisfiable core of the .cnf as a bag of literals -- i.e.
		 * ignoring the clause structure and just looking at the literals that
		 * are mentioned in the core.
		 * <p>
		 * Some literals have semantic meaning in terms of the translatable AST.
		 * Each literal is either a Boolean variable allocated to a relation (or
		 * the negation of such a Boolean variable), or a literal allocated to
		 * some node of the ground Boolean DAG. Some nodes of the ground Boolean
		 * DAG are instantiations of a given Boolean template with given
		 * arguments; so are the Boolean literals allocated to these nodes in
		 * the Plaisted-Greenbaum scheme of converting the Boolean DAG to CNF.
		 * The information on which literals represent the instantiation of
		 * which Boolean templates has been written to an .ist file when the
		 * .cnf file was created from the .sat file by sat2cnf.
		 * <p>
		 * We now run the program getAstStencil which looks at which literals
		 * are in the cnf unsat core, which Boolean template instantiations they
		 * represent, and writes out a stencil file which says which Boolean
		 * template instantiations are used in the core. We read the stencil
		 * from that file and return it.
		 */

        //System.out.println("constructing the stencil...");
		final File istFileHandle = BLBackend.getLastIstFileHandle();
		final File stencilFileHandle = TmpFiles.createHandleToATempFile("clauses.stc");

        //UcoreProofProcessor (Java) replaces getAstStencil (C++)
		if (Params.glob.getBoolParam("DEVEL", "JavaUcore")) {
			//Dbg.info("Processing extracted unsat core. (using the replacement Java implementation)...");
			UcoreProofProcessor processor = new UcoreProofProcessor();
			processor.getAstStencil(lastCnfFileHandle, istFileHandle, stencilFileHandle);
		} else {
			//Dbg.info("Processing extracted unsat core. (using old C++ implementation)...");
			final String[] args = {
					lastCnfFileHandle.getName(),
					istFileHandle.getName(),
					stencilFileHandle.getName(),
					Integer.toString(curIter)
					};
			ProcessInfo.runTillEnd("getAstStencil", args, TmpFiles.getTmpDir());
		}
		//Dbg.info("Unsat core processing complete.");
		//checkCore(stencilFileHandle, coreFileHandle);
		//cleanupCoreFiles(lastCnfFileHandle, curIter);

		// read the Boolean stencil written by the program getAstStencil,
		// and return it.
		return new BoolStencil(stencilFileHandle);
    	} catch (IOException ioe_) {
    		Dbg.fatal("I/O exception when determining unsat core", ioe_);
    		throw new RuntimeException(ioe_);
    	}
    } // computeUnsatCore()

/**
 * called only by BoolStencil (defined above)
 * 
 * Verify that re-grounding-out with the stencil will yield a superset of the
 * core by regrounding and checking that we get a superset of the unsat core.
 * 
 * @param stencilFileHandle
 * @param coreFileHandle
 */
  protected void checkCore(final File stencilFileHandle, final File coreFileHandle) {
  //System.out.println("regrounding to verify core...");
  File regroundCnfFileHandle = TmpFiles.createHandleToATempFile("reground.cnf");
  File regroundIstFileHandle = TmpFiles.createHandleToATempFile("reground.ist");
  try {
  	final String[] sat2cnfArgs = {
			"-t", ".", //TmpFiles.getTmpDir().toString(),
			"-n", regroundIstFileHandle.getName(),
			"-m", Long.toString(Params.glob.getLongParam("MAIN", "maxCMem", 20000)),
			(Params.glob.getBoolParam("MAIN", "multsol", true) ? " -e " : ""),
			"-s" + stencilFileHandle.getName(),
			BLBackend.getLastSatFileHandle().getName(),
			regroundCnfFileHandle.getName()};
      _process =
      new SATProcessInfo("sat2cnf", sat2cnfArgs, TmpFiles.getTmpDir());
  } catch (IOException ioe_) { Dbg.fatal("could not start zchaff", ioe_); }
  _process.runUntilOutcome();
  _killProcess();
  //System.out.println("regrounding done.");

  // Test that each clause in iterFileName (the unsat core) is also in reground.cnf
	try {
		Set /* of String */coreClauses = new HashSet();
		LineNumberReader iterReader = new LineNumberReader(
				new BufferedReader(new FileReader(coreFileHandle)));
		String line = null;

		while ((line = iterReader.readLine()) != null) {
			if (!(line.startsWith("c ") || line.startsWith("p cnf ")))
				coreClauses.add(line.trim());
		}
		iterReader.close();

		Set /* of String */regroundClauses = new HashSet();
		iterReader = new LineNumberReader(new BufferedReader(
				new FileReader(regroundCnfFileHandle)));
		line = null;
		Dbg.chk(iterReader.readLine().startsWith("c maxindep "));
		Dbg.chk(iterReader.readLine().startsWith("p cnf "));
		while ((line = iterReader.readLine()) != null) {
			regroundClauses.add(line.trim());
		}
		iterReader.close();

		//System.out.println(coreClauses.size() + " core clauses");
		//System.out.println(regroundClauses.size() + " reground
		// clauses");

		//System.out.println("checking subset...");
		int clausesOk = 0;
		for (Iterator coreClauseIter = coreClauses.iterator(); coreClauseIter
				.hasNext();) {
			String coreClause = (String) coreClauseIter.next();
			// if (!regroundClauses.contains(coreClause))
			//     System.out.println("core clause MISSING: " + coreClause);
			if (regroundClauses.contains(coreClause))
				clausesOk++;
		}
		//System.out.println(clausesOk + " clauses ok.");
		//System.out.println("subset check finished.");
	} catch (IOException ioe_) {
		Dbg.fatal("sanity check failed: ", ioe_);
	}
  }

    /**
	 * called only by BoolStencil.
	 * redundant since the directory containing these temp files is deleted upon exit.
	 * 
	 * @param lastCnfFileHandle
	 * @param curIter
	 */
  protected void cleanupCoreFiles(final File lastCnfFileHandle, final int curIter) {
  	for (int i=0; i<=curIter; i++) {
  		String delIterFileName = lastCnfFileHandle + "_iteration_" + i;
  		FileUtil.move(delIterFileName, delIterFileName + ".old");
  		//System.out.println("deleted " + delIterFileName);
  	}
  }

    /**
     * Prints a message to Dbg.warn stream stating which platform specific
     * binary failed to execute, sets _lastResult to BL_ERR and throws an EnvFailureException
     * @param component name of the file that couldn't be executed
     **/
    private void envFailure(String component) throws EnvFailureException {

	_lastResult = BL_ERR;

	Dbg.warn("Alloy Analyzer has encountered difficulties running the platform specific binaries for "+
                 component + ".  The Analyzer will not be able to execute your model until this issue " + 
		 "is resolved.  Please see the Alloy website (http://alloy.mit.edu) for help with "+ 
		 "troubleshooting common problems.");

	throw new EnvFailureException("Could not execute " + component);
    }

    boolean _extractingUnsatCore = false;

    BooleanFormula _ucore_formula;
    int _ucore_nvars;
    boolean[] _ucore_dependentVars;
    long _ucore_randSeed;
    File _ucore_primVarFileHandle;

  /**
   * Solve a .sat instance.
   *
   * This method can take a long time to return, so should not be called
   * from the Swing event thread.
   *
   * @param formula_ the {@link BooleanFormula} we are solving
   * @param nvars_ number of Boolean variables in the formula_
   * @param dependentVars_ for each boolean variable, whether it is dependent;
   *                       for a given combination of independent variable values,
   *                       at most one setting of the dependent variables gives
   *                       a satisfiable assignment.
   * @param solverName_ which SAT solver to use
   * @param enum_ whether to support solution enumeration.
   * @param randSeed_ seed for the pseudorandom number generator, passed on to the SAT solver
   *
   * @return {@link #BL_UNSAT}, {@link #BL_SAT}, {@link #BL_CANCELLED}, or {@link #BL_ERR}.
   *         If {@link #BL_SAT} is returned, {@link #getLastSolution} may be called to
   *         retrieve the satisfying assignment, and {@link #next} may be called to
   *         enumerate subsequent satisfying assignment.
   */
  protected int _solve(BooleanFormula formula_,
               int nvars_, boolean[] dependentVars_,
               String solverName_,
               boolean enum_,
               long randSeed_,
               int runType_,  // BL_RUN_SOLVE/BL_RUN_COUNT/BL_RUN_VARORDER
               File primVarFileHandle_
               ) throws EnvFailureException {

      _ucore_formula = formula_;
      _ucore_nvars = nvars_;
      _ucore_dependentVars = dependentVars_;
      _ucore_randSeed = randSeed_;
      _ucore_primVarFileHandle = primVarFileHandle_;

    // The solver process may still be running, if we were enumerating
    // solutions to the previous problem.  Since we're now starting
    // a new problem, kill the solver first.
    if (_process!=null && _process.isRunning()) _killProcess();

    //
    // Write the SAT formula to a .sat file
    //

    File satFileHandle = TmpFiles.createHandleToATempFile("clauses.sat");
    File cnfFileHandle = TmpFiles.createHandleToATempFile("clauses.cnf");
    File solutionFileHandle = TmpFiles.createHandleToATempFile("solution.slv");

    // the Boolean template instantiation file, written by sat2cnf:
    // for each variable of the resulting CNF that was allocated
    // to a node of the ground Boolean DAG, sat2cnf tells us about that node --
    // which Boolean template the node instantiates, and with which arguments.
    File istFileHandle = TmpFiles.createHandleToATempFile("clauses.ist");

    _lastNumVars = nvars_;
    _lastSolutionFileHandle = solutionFileHandle;
    _lastCnfFileHandle = cnfFileHandle;
    _lastIstFileHandle = istFileHandle;
    _lastSatFileHandle = satFileHandle;
    int outcome;
//     if (Params.glob.getBoolParam("DEVEL","javacnf")) {
//       formula_.writeCNF(cnfFileName, nvars_);
//     } else
    {
      formula_.writeSatFile(satFileHandle, nvars_, dependentVars_);
      //
      // Convert the .sat file to a .cnf file, by running
      // the sat2cnf external program
      //

      // start up sat2cnf
      try {
	  boolean supportUcore = _extractingUnsatCore; //Params.glob.getBoolParam("MAIN", "ucore", false);
      	final String[] args = {
			"-t", ".", //TmpFiles.getTmpDir().toString(),
			supportUcore ? "-n" : "", supportUcore ? istFileHandle.getName() : "",
			"-m", Long.toString(Params.glob.getLongParam("MAIN", "maxCMem", 20000)),
			(enum_ == ENUM_ON ? " -e " : ""),
			satFileHandle.getName(),
			cnfFileHandle.getName()
			};
        _process = new SATProcessInfo("sat2cnf", args, TmpFiles.getTmpDir());
      } catch (IOException ioe_) { 
          //Dbg.fatal("could not start sat2cnf", ioe_); 
	  envFailure("sat2cnf");
      }
      _process.runUntilOutcome();
      _killProcess();  // i.e. kill sat2cnf

      outcome = _process.getOutcome();
      if (outcome != SATProcessInfo.NORMAL_TERMINATION) {
    // then outcome is one of:
    // CANCELLED_BY_USER, ENVIRONMENTAL_ERROR, INTERNAL_ERROR.
    // in all of these cases, we immediately return.
    if (outcome == SATProcessInfo.CANCELLED_BY_USER)
          return _lastResult = BL_CANCELLED;
    if (outcome == SATProcessInfo.ENVIRONMENTAL_ERROR) {
	envFailure("sat2cnf");
    }
    if (outcome == SATProcessInfo.INTERNAL_ERROR) {
	envFailure("sat2cnf");
    }
      }  // if (outcome != NORMAL_TERMINATION)
    }

    if (_extractingUnsatCore)
	return BL_UNSAT;  // anything other than BL_CANCELLED

    //
    // Solve the CNF formula
    //

    // If the solution file exists, delete it -- this is so if
    // the solver crashes, we don't confuse a leftover solution
    // file for the current solution.

    //solutionFileHandle.delete();
    //solutionFileHandle = TmpFiles.createHandleToATempFile("solution.slv");

    // one of the solvers, mchaff, requires a config file --
    // extract it from the .jar to the temp dir if not there already
    File mchaffConfigFileHandle = null;
    if (solverName_.equals("MCHAFF")) {
      try { mchaffConfigFileHandle = ResourceManager.getResource("mchaff.smj"); }
      catch (IOException ioe_) { 
	  Dbg.warn("Could not extract mchaff.smj");
	  envFailure("mchaff"); 
      }
    }

    long enumBatchSize = Params.glob.getLongParam("MAIN", "enumBatchSize", 1);
    String solver = solverName_.equals("MCHAFF") ? "mchaff" :
    (solverName_.equals("ZCHAFF") ? "zchaff" :
     (solverName_.equals("RELSAT") ? "relsat" :
      (solverName_.equals("BERKMIN") ? "berkmin" :
       (solverName_.equals("LIMMAT") ? "limmat" :
	(solverName_.equals("MINISAT") ? "minisat" : null)))));
    try {
    	final String[] args = {
			"-s", solutionFileHandle.getName(),
			"-r", Long.toString(randSeed_),
			(primVarFileHandle_==null ? "" : "-p " + primVarFileHandle_.getName()),
			(enumBatchSize==1 ? "" : ("-b " + enumBatchSize)),
			"-i", Long.toString(Params.glob.getLongParam("MAIN", "progressInterval", 4)),
			(runType_==BL_RUN_VARORDER ? "-t" : ""),
			(runType_==BL_RUN_COUNT ? "-#" : ""),
			(Params.glob.getBoolParam("MAIN","primsplit",false) ? "-1" : ""),
			cnfFileHandle.getName(),
			(mchaffConfigFileHandle == null ? "" : mchaffConfigFileHandle.getName())
			};
      _process =
      new SATProcessInfo(solver, args, TmpFiles.getTmpDir());
    } catch (IOException ioe_) { envFailure(solver); }

    _process.runUntilOutcome();

    outcome = _process.getOutcome();
    if (outcome != SATProcessInfo.NORMAL_TERMINATION) {
      // then outcome is one of:
      // CANCELLED_BY_USER, ENVIRONMENTAL_ERROR, INTERNAL_ERROR.
      // in all of these cases, we immediately return.
      _killProcess();
      if (outcome == SATProcessInfo.CANCELLED_BY_USER)
        return _lastResult = BL_CANCELLED;
      if (outcome == SATProcessInfo.ENVIRONMENTAL_ERROR) {
	  envFailure(solver);
      }
      if (outcome == SATProcessInfo.INTERNAL_ERROR) {
	  envFailure(solver);
      }
    }  // if (outcome != NORMAL_TERMINATION)

    //
    // outcome==NORMAL_TERMINATION: solver has written the result
    // into the file whose name is in solutionFileName.  but what
    // is written depends on the type of run we were doing (runType).
    //
    // if runType_==BL_RUN_SOLVE, solution file contains solution(s) to CNF.
    // if runType_==BL_RUN_COUNT, solution file contains the solution count
    // if runType_==BL_RUN_VARORDER, solution file contains the list of variables
    //                               set early in the run.
    //

    try {
      _solReader = new LineNumberReader(new FileReader(solutionFileHandle), 32768);
    } catch (IOException ioe_) { Dbg.fatal("Could not open solution file", ioe_); }

    if (runType_==BL_RUN_SOLVE) {
      _readAssignmentFrom(_solReader, nvars_);
      // do not close _solReader here: we may be reading solutions in batches,
      // and there may be more solutions in the solution file.
    } else if (runType_ == BL_RUN_VARORDER) {
      _readVarOrderFrom(_solReader);
    } else if (runType_ == BL_RUN_COUNT) {
      _readSolCountFrom(_solReader);
    }

    if (!(_lastResult == BL_SAT && canEnumerateSolutions(solverName_)))
      _killProcess();
    return _lastResult;
  }  // _solve()


  /**
   * If the solver or sat2cnf process is running, kill it by sending it a "0" command to its stdin.
   */
  protected void _killProcess() {
    if (_process == null || !_process.isRunning()) return;
    _process.sendLine("0");
    _process.waitForTermination();
    if (_solReader != null) {
      try { _solReader.close(); } catch (IOException ioe_) {
	  Dbg.warn("Could not close solution file", ioe_);
      }
      _solReader = null;
      //_lastSolutionFileHandle.delete();
    }
  } // _killProcess()


  /**
   * Get next solution, if last solve() returned BL_SAT
   */
  protected int _next() {
    if (_lastResult != BL_SAT) return _lastResult;

    //
    // Solutions are returned by the solver in batches
    // of size specified by the global parameter MAIN.enumBatchSize.
    // Here, we see if there is another solution in the current
    // batch; if yes, return it, if no, ask the solver
    // for another batch of solutions.
    //

    _readAssignmentFrom(_solReader, _lastNumVars);
    if (_lastResult != BL_ENDBATCH)
      return _lastResult;

    // no more solutions in batch: ask the solver for another batch.
    try { _solReader.close(); }
    catch(IOException ioe_) {
      Dbg.warn("Could not close solution file", ioe_);
    }
    _lastSolutionFileHandle.delete();
    _solReader = null;

    _process.runUntilOutcome(new Runnable() { public void run() {
      // tell the solver to give us the next batch of solutions
      _process.sendLine("1");
    }});
    try {
      _solReader = new LineNumberReader(new FileReader(_lastSolutionFileHandle), 32768);
    } catch (IOException ioe_) {
      Dbg.fatal("Could not open solution file", ioe_);
    }

    _readAssignmentFrom(_solReader, _lastNumVars);
    return _lastResult;
  }  // _next()

  /**
   * Cause a currently running {@link #solve} or {@link #next} to quit immediately,
   * returning {@link #BL_CANCELLED}.
   */
  protected void _interruptSolver() {
  	_cancelInProgress = true;
    if (_cancelInProgress)
    		Dbg.info("Aborting last command...");
    else	Dbg.info("Not aborting last command...this may mean trouble...");
  	if (_process != null)
  		_process.sendLine("0");
  }

  /**
   * clean up temporary files created during this session
   * 
   * TODO this should probably do something
   */
  private synchronized void _cleanUpTempFiles() {}

  /**
   * Check the environment to make sure all the necessary files
   * are present, the temporary directory is writeable, etc.
   * If there is a problem, returns a {@link String} error message;
   * otherwise returns <code>null</code>.
   * 
   * TODO this should probably do more than just return null
   */
  protected String _checkEnvironment() { return null; }

    protected File _getLastCnfFileHandle() { return _lastCnfFileHandle; }
    protected File _getLastIstFileHandle() { return _lastIstFileHandle; }
    protected File _getLastSatFileHandle() { return _lastSatFileHandle; }
}  // class BLSATLab
